モノイダル圏の定義 フルバージョン

code:MonoidalCategory.sig

2-signature

<MonCAT: c; m, i; α, λ, ρ>

fixed-in <: CAT; ×, I>

Data

0-morph underlying @ c : CAT

1-morph product @ m : c × c -> c

1-morph unit @ i : I -> c

2-iso associator @ α

: (m × c^) * m => (c^ × m) * m

: c × c × c -> c

2-iso l-unitor @ λ

: (i × c^) * m => c^

: c -> c

2-iso r-unitor @ ρ

: (c^ × i) * m => c^

: c -> c

Axioms

3-eq triangle-identity

: (ρ × c^) * m =3= (c^ × i × c^) * α ; (c^ × λ) * m

: (c^ × i × c^) * (m × c^) * m => m

: c × c -> c

3-eq pentagon-identity

: (m × c^ × c^) * α ; (c^ × c^ × m) * α =3= (α × c^) * m ; (c^ × m × c^) * α ; (c^ × α) * m

: (m × c^ × c^) * (m × c^) * m => (c^ × c^ × m) * (c^ × m) * m

: c × c × c × c -> c

$ \left\lang\mathrm{ MonCAT }\colon c; m, i; α, λ, ρ \right\rang

where

$ \forall a,b,c\colon \mathbf{CAT}

$ (a,b,c).\dot α \colon (a×b)× c → a×(b×c)

$ a.\dot λ \colon I × a → a

$ a.\dot ρ \colon a × I → a

0-morph

1-morph

$ m =(\otimes)\colon c×c\to c

$ i \colon I → c

2-iso

$ α \colon (m × c^\wedge) * m

$ ⇒ (c,c,c).\dot α * (c^\wedge × m) * m

$ \colon (c×c)×c → c

$ λ\colon (i × c^\wedge) * m ⇒ c.\dot λ

$ \colon I × c → c

$ ρ\colon (c^\wedge × i) * m ⇒ c.\dot ρ

$ \colon c × I → c

公理系

https://gyazo.com/2d529f59c37b1e6321188faef7b319c8

https://gyazo.com/1bd18013dd521cfd063fd26553eab70f

$ (ρ × c^\wedge) * m

$ = ((c^\wedge × i) × c^\wedge) * α

$ ; (c,I,c).\dot α * (c^\wedge × λ) * m

$ \colon ((c^\wedge × i) × c^\wedge) * (m × c^\wedge) * m

$ ⇒ (c,c).\mathrm{Tri} * m

$ : (c × I) × c → c

where

$ (c,i,c).\dot α

$ = ((c^\wedge × i) × c^\wedge) * (c,c,c).\dot α

$ = (c,I,c).\dot α * (c^\wedge × (i × c^\wedge ))

$ (c,c).\mathrm{Tri} \coloneqq c.\dot ρ × c^\wedge

$ = (c,I,c).\dot \alpha * (c^\wedge \times c.\dot \lambda)

$ \colon (c × I) \times c \to c\times c

WIP.icon

https://gyazo.com/f5a15e8b75c90559a4e104ec8d0261ae

$ (m × c^\wedge × c^\wedge) * α

$ ; (c^\wedge × c^\wedge × m) * α

$ = (α × c^\wedge) * m

$ ; (c^\wedge × m × c^\wedge) * α

$ ; (c^\wedge × α) * m

$ \colon (m × c^\wedge × c^\wedge) * (m × c^\wedge) * m

$ ⇒ (c^\wedge × c^\wedge × m) * (c^\wedge × m) * m

$ \colon c × c × c × c → c